\begin{tabbing}
$\vdash$  \=$\forall$$T$:Type, $x$, $y$:$T$, $L_{1}$, $L_{2}$:($T$ List).\+
\\[0ex]adjacent($T$;$L_{1}$ @ $L_{2}$;$x$;$y$)
\\[0ex]$\Leftarrow\!\Rightarrow$ \=(adjacent($T$;$L_{1}$;$x$;$y$)\+
\\[0ex]$\vee$ ((0 $<$ $\parallel$$L_{1}$$\parallel$) \& (0 $<$ $\parallel$$L_{2}$$\parallel$) \& $x$ = last($L_{1}$) \& $y$ = hd($L_{2}$))
\\[0ex]$\vee$ adjacent($T$;$L_{2}$;$x$;$y$))
\-\-
\end{tabbing}